ArghDA M3 follow-on: workspace-fed verdicts + staleness in reason#43
Merged
Merged
Conversation
The Flying-Logic reasoning graph can now source REAL prover verdicts from a four-state workspace's `proven/` state without re-running any tool, and demote a stale-proven node back to unknown — honest by construction, never fabricated. - `reason::workspace_verdicts(dag, proven, stale)` — pure mapping: a node whose file basename is in the workspace's `proven/` set → Proven; if that same file is stale (content/closure hash changed since promotion) it is added to the stale set, so the existing demote-only fold lowers it to Unknown. Matched by file basename (documented collision caveat). Re-exported from lib.rs. - `arghda reason <path> --workspace <ws>`: reads the proven + stale-proven basename sets off the workspace (Workspace::list / stale_proven) and feeds them in. `--check` stays authoritative — a fresh typecheck overrides the workspace verdict and clears staleness for that node. - Evidence strings are honest: "prover: proven" for a fresh promotion, "prover: proven; stale: closure hash changed" for a demoted stale one. Verification: `cargo fmt --check`, `cargo clippy --all-targets -- -D warnings`, `cargo test` (130 pass, +1 reason unit), `check-spdx.sh` all green. Dogfooded end-to-end: fresh proven leaf → effective proven, un-proven root → unknown; editing the proven file on disk → node demoted to unknown with the stale evidence string. Completes the refinement follow-ons bucket (M4 .ipkg roots, M6 axiom audit, M3 workspace verdicts). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
hyperpolymath
marked this pull request as ready for review
July 1, 2026 10:58
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
The Flying-Logic reasoning graph can now source real prover verdicts from a four-state workspace's
proven/state without re-running any tool, and demote a stale-proven node back tounknown. Honest by construction — a verdict only ever comes from a recorded promotion, and staleness always dominates a staleProven.This is the last of the three refinement follow-ons (M4
.ipkgroots #41, M6 axiom audit #42, M3 workspace verdicts).How
reason::workspace_verdicts(dag, proven, stale) -> (verdicts, stale)— a pure mapping (no I/O, unit-testable): a node whose file basename is in the workspace'sproven/set →Proven; if that same file is stale (content/closure hash changed since promotion) it is added to the returned stale set, so the existing demote-only fold lowers it toUnknown. Matched by file basename (documented collision caveat). Re-exported fromlib.rs.arghda reason <path> --workspace <ws>— reads the proven + stale-proven basename sets off the workspace (Workspace::list(Proven)/Workspace::stale_proven) and feeds them intoworkspace_verdicts.--checkstays authoritative: a fresh typecheck overrides the workspace verdict and clears staleness for that node."prover: proven"for a fresh promotion;"prover: proven; stale: closure hash changed"for a demoted stale one.Verification (actually run)
cargo fmt --check— cleancargo clippy --all-targets -- -D warnings— cleancargo test— 130 pass (+1 reason unit: proven lights the cone, stale demotes)bash scripts/check-spdx.sh .— OKDogfooded end-to-end on a real workspace + Agda source tree:
Good→effective: proven("prover: proven"); un-proven rootAll→unknown.Gooddemoted tounknownwith"prover: proven; stale: closure hash changed".Scope
Additive only.
M3base was already 100%; this refinement wires the reasoning graph to the triage workspace's ground truth. No change to thereason/0.1JSON contract keys.🤖 Generated with Claude Code
https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
Generated by Claude Code